Formale Methoden zur Entwicklung korrekter Software

Projektleitung und Mitarbeiter

Klaeren, H. (Prof. Dr. rer. nat.), Schmitz, Ch. (Dipl. Inform.)

Mittelgeber :

Forschungsbericht : 1994-1996

Tel./ Fax.:

Projektbeschreibung

Algebraische Spezifikationen sind ein sehr gut geeignetes Mittel, um die funktionalen Anforderungen an ein Programm formal zu beschreiben. Wir betrachten Methoden zur Spezifikation und korrekten Implementierung von objektorientierten bzw. imperativen Programmen. Dabei wird insbesondere untersucht, wie im applikativen Rahmen algebraischer Spezifikationen der Programmzustand adäquat modelliert und behandelt werden kann. Dies soll durch die axiomatische Beschreibung eines Speichermodells erreicht werden. Weitere Schwerpunkte bilden die Frage nach geeigneten Implementierungsbeweisen und die Anwendung dieser Verfahren auf größere Programme.

Publikationen

Schmitz, Chr.: Korrektheitsbeweis objektorientierter Programme durch formale betrachtungsorientierte Spezifikationen. In: Simon, F. (ed.), Alternative Konzepte für Sprachen und Rechner, Bad Honnef 1994, Bericht Nr. 9412, Christian-Albrechts-Universität Kiel, 1994.

INDEX HOME SUCHEN KONTAKT LINKS

qvf-info@uni-tuebingen.de(qvf-info@uni-tuebingen.de) - Stand: 30.11.96
Copyright Hinweise